| Definitions | t  T, s = t, x:A  B(x),  x:A. B(x), E(X), type List, ES, AbsInterface(A), Id, loc-on-path(es;i;L),  A, x:A  B(x), P & Q,  x:A. B(x), P   Q, Top, [], E, P  Q, P Q, False, A List ,  , e  X, S  T, State(ds), State(ds), state@i, vartype(i;x), f(x)?z, f g, constant_function(f;A;B), r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),   x,y. t(x;y), x. t(x), Knd, EState(T), f(a), EOrderAxioms(E; pred?; info), IdLnk, Unit, EqDecider(T), Type, A c B, (last change to x before e), lastchange(x;e), t.1, let x,y = A in B(x;y), isrcv(e), isrcv(k), es-first-from(es;e;l;tg), kind(e), es-init(es;e), destination(l), source(l), {T}, <a, b>, a:A fp B(a), loc(e),  , as @ bs, [car / cdr], (x l), Atom$n, {x:A| B(x)} ,  b, P  Q, left + right, Void, strong-subtype(A;B), e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), e c e', (e < e'), e loc e' , (e <loc e'), MaName, l_disjoint(T;l1;l2), Dec(P), kind(e), loc(e) |